\begin{tabbing}
$\forall$\=$D$:Dsys, ${\it sched}$:(Id$\rightarrow$($\mathbb{N}\rightarrow$(IdLnk+Id)+Unit)), $v$:($i$:Id$\rightarrow$M($i$).state),\+
\\[0ex]${\it dec}$:($i$,$a$:Id$\rightarrow$M($i$).state$\rightarrow$(M($i$).da(locl($a$))+Unit)), $l$:IdLnk.
\-\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ $\neg$M(source($l$)) sends on link $l$
\\[0ex]$\Rightarrow$ ($\forall$$t$:$\mathbb{N}$. queue($l$;$t$) $=$ nil $\in$ Msg($\lambda$$l$,${\it tg}$. M(source($l$)).dout2($l$;${\it tg}$)) List)
\end{tabbing}